Lambda the Ultimate

A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language

I present a certified compiler from simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. I demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge automatically large parts of the proof obligations.

Software/proof source code and documentation

Slides are available from a talk I gave at the Projet Gallium seminar at INRIA Rocquencourt, in OpenOffice and PDF formats.

I found this while attempting to follow up on this post. The approach taken here—dependently-typed ASTs and denotational semantics—and the observation that, carried to its logical conclusion, the result is typed intermediate and assembly languages, proof-carrying code, etc. suggests to me a connection to this work. It also seems to offer a denotational counterpoint to Leroy's coinductive big-step operational semantics, also done in Coq. Fascinating stuff.

We are pleased to announce the Twelf Wiki, a major new source of documentation about Twelf:

http://twelf.plparty.org

Twelf is a tool used to specify, implement, and prove properties of deductive systems. The Twelf Wiki includes:

• A new introduction to LF and Twelf.
• Tutorials on common Twelf tricks and techniques.
• Case studies of larger applications of Twelf, including encodings of and proofs about linear logic, mutable state, and CPS conversion.
• Pre-compiled CVS builds of Twelf for Linux and Windows.

We invite you to come share what you know, learn from what's there, and ask questions about what's not.

- The Twelf Wiki Team

(I know many of the people working on this, and they've put in a lot of effort to make a really useful resource.)

I am a little late in passing on these news, but the new ISO standard for Ada is now officially published.

We discussed the new features in this revision of the language a couple of times before, so search the archives if you are interested. Among the new things are interface (as in Java), a container library, and the ability to use the "distinguished receiver" or prefix style in method calls.

For the record, the the recommended informal name for the latest Ada standard is Ada 2005, not Ada 2007.

A Topos Foundation for Theories of Physics: I. Formal Languages for Physics. Andreas Döring and Chris Isham.

This paper is the first in a series whose goal is to develop a fundamentally new way of constructing theories of physics. The motivation comes from a desire to address certain deep issues that arise when contemplating quantum theories of space and time. Our basic contention is that constructing a theory of physics is equivalent to finding a representation in a topos of a certain formal language that is attached to the system. Classical physics arises when the topos is the category of sets. Other types of theory employ a different topos. In this paper we discuss two different types of language that can be attached to a system, S. The first is a propositional language, PL(S); the second is a higher-order, typed language L(S). Both languages provide deductive systems with an intuitionistic logic. The reason for introducing PL(S) is that, as shown in paper II of the series, it is the easiest way of understanding, and expanding on, the earlier work on topos theory and quantum physics. However, the main thrust of our programme utilises the more powerful language L(S) and its representation in an appropriate topos.

This is a little outside of our usual areas, but I think it will appeal to at least some readers. Personally, I find the approach aesthetically very, very appealing for several reasons, and I would be thrilled if an answer to quantum cosmology came from this direction, but I'm the first to admit that my grasp of the phsyics is barely enough to follow along. I was able to make it through this paper fairly easily, but things aren't too interesting in the classical case, and I sadly suspect that the application to quantum physics in parts II and III will leave me behind.

Via The n-Category Cafe, where there is also considerable discussion, much of it around the single word "peristalithic"...

John Backus, inventor of FORTRAN, the BNF, and winner of the 1977 Turing Award, has passed away. New York Times has an obituary. I'm sure the more eloquent members of LtU will have much to say about him, so I'll just point out that his Turing Award lecture is an absolute classic, and seems to be more relevant than ever. My condolences to the Backus family and friends.

An Intensional Type Theory: Motivation and Cut-Elimination, Paul C. Gilmore.

By the theory TT is meant the higher order predicate logic with the following recursively defined types:

(1) 1 is the type of individuals and [] is the type of the truth values;
(2) [Ï„1, ..., Ï„n] is the type of the predicates with arguments ofthe types Ï„1, ..., Ï„n.

The theory ITT described in this paper is an intensional version of TT. The types of ITT are the same as the types of TT, but the membership of the type 1 of individuals in ITT is an extension of the membership in TT. The extension consists of allowing any higher order term, in which only variables of type 1 have a free occurrence, to be a term of type 1. This feature of ITT is motivated by a nominalist interpretation of higher order predication. In ITT both well-founded and non-well-founded recursive predicates can be defined as abstraction terms from which all the properties of the predicates can be derived without the use of non-logical axioms.

The elementary syntax, semantics, and proof theory for ITT are defined. A semantic consistency proof for ITT is provided and the completeness proof of Takahashi and Prawitz for a version of TT without cut is adapted for ITT; a consequence is the redundancy of cut.

Russell showed Frege's original foundations of mathematics inconsistent when he invented Russell's paradox -- does the set of all sets that do not contain themselves contain itself? This paradox arises because Frege's logic contained an unrestricted comprehension principle -- you could create a set from any predicate. This allows you to cook up vicious cycles such as in Russell's paradox, and the traditional method (invented by Russell) for avoiding these cycles is to allow quantification in a predicative hierarchy: when you comprehend a predicate at level i, you create a set at level i+1, and a predicate at a given level can never mention sets at a higher level.

This paper claims that you can allow unrestricted impredicative quantification if you keep careful track of Frege's sense-reference distinction, and distinguish between predicates and names of predicates. This (if it really works -- I haven't done more than skim the paper yet) would be a different method of using a predicative hierarchy to avoid the paradoxes.

Google Summer of Code 2007 is now on. Among the projects suggested by mentoring organizations, quite a few may be of interest to language hackers.

Here are some organizations that have interesting (language oriented) project ideas: Boost C++, Haskell.org, Jikes RVM, LLVM, PHP and Python.

For some reason (probably starting with the letter N), seperation logic was recently mentioned here a few times. Since this area may be relatively unknown to many readers, I thought the following two course web sites from John C. Reynolds may be of interest:

Separation Logic (Spring 2004)

Current Research on Separation Logic (Spring 2005)

Pico Lisp: A Radical Approach to Application Development describes a minimalist Lisp interpreter which has been used to build real applications for ~20 years. If you ignore the tendency toward self-aggrandizing, there's some food for thought here. Pico Lisp only has native support for symbols, integers, and lists (no arrays, no structures), and is implemented as a straightfoward interpreter. Yet in the benchmarks (usual disclaimers here), Pico Lisp fares well against a compiled Lisp. Is there a case to be made for ultra lean and mean interpreters as a viable alternative to compilers?

Scalable Statistical Bug Isolation, Ben Liblit, Mayur Naik, Alice X. Zheng, Alex Aiken, Michael I. Jordan.

We present a statistical debugging algorithm that isolates bugs in programs containing multiple undiagnosed bugs. Earlier statistical algorithms that focus solely on identifying predictors that correlate with program failure perform poorly when there are multiple bugs. Our new technique separates the effects of different bugs and identifies predictors that are associated with individual bugs. These predictors reveal both the circumstances under which bugs occur as well as the frequencies of failure modes, making it easier to prioritize debugging efforts. Our algorithm is validated using several case studies, including examples in which the algorithm identified previously unknown, significant crashing bugs in widely used systems.

This work is reminiscent of Daikon.